#include <klee/klee.h>
#include <stdlib.h>
#include <string.h>
#include <stdio.h>
#include <assert.h>
#include <time.h>

#define bool int
#define true 1
#define false 0


#define IdNotValidated -2
#define TableMaxRow 10

#define OK 0

#define ErrOutOfTableMaxRow 1
#define ErrBreakTableConstraint 2




#define STR_MAX_LEN 12

//{table Activity :  java or mysql.table or sql
#define Score1 3 
#define Score2 29
#define Score3 7 
#define Score4 31 
#define ScoreNotValidated1 -101
#define ScoreNotValidated2 -103

#define ActivityTypeNull 0
#define FirstId 1

struct _Activity {
	int id;
	char name[STR_MAX_LEN];
	bool on;//0,1
	int newUserScore;//3
	int oldUserScore;//11
	int shopId;//0:NULL,1,2,3
};

typedef struct _Activity Activity;

Activity* activityTab[TableMaxRow];
int activityTabCurIndex = -1;
int activityTabCurId = FirstId;

void printRow_activity(Activity * pa,char* msg) {
	printf(" %s :: activity: {id:%d, name:%s, shopId:%d, on:%d, newUserScore:%d, oldUserScore:%d} ; \n", msg,pa->id, pa->name, pa->shopId, pa->on, pa->newUserScore, pa->oldUserScore   );
}

int internalCheckTableValidated_activity() {
	for (int i = 0; i <= activityTabCurIndex - 1; i++) {
		for (int k = i + 1; k <= activityTabCurIndex; k++) {
			assert (activityTab[i]->id != activityTab[k]->id);// non repeated id
			assert (strcmp(activityTab[i]->name, activityTab[k]->name) != 0) ; // non repeated name
		}
	}
	return true;
}

Activity* sql_selectOneRowFromTableWhere_activity_shopId(int shopId){
	for (int i = 0; i <= activityTabCurIndex - 1; i++) {
			if (activityTab[i]->shopId == shopId){
                return activityTab[i];
            }
	}
	return NULL;
}

void sql_selectTable_activity_print(){
    printf("sql_selectTable_activity_print__[\n");
	for (int i = 0; i <= activityTabCurIndex ; i++) {
        printRow_activity(activityTab[i],"sql_selectTable_activity_print");
	}
    printf("]\n");
}
//}

//{table User : may generate from java or mysql.table 
#define UserTableMaxRow 10

struct _User {
	int id;
	char phone[STR_MAX_LEN];
	int shopId;//0:NULL,1,2,3
};

typedef struct _User User;

User* userTab[TableMaxRow];
int userTabCurIndex = -1;
int userTabCurId = FirstId;

void printRow_user(User * p,char* msg) {
    if(p==NULL){
        printf("%s:null\n",msg);
    }else{
        
	printf(" %s :: user: {id:%d, phone:%s, shopId:%d } ; \n", msg,p->id, p->phone , p->shopId);
    }
}

int internalCheckTableValidated_user() {
	for (int i = 0; i <= userTabCurIndex - 1; i++) {
        // printRow_user(userTab[i],"internalCheckTableValidated_user_loop");
		for (int k = i + 1; k <= userTabCurIndex; k++) {
            // printRow_user(userTab[i],"internalCheckTableValidated_user_i");
            // printRow_user(userTab[k],"internalCheckTableValidated_user_k");
			assert (userTab[i]->id != userTab[k]->id);// non repeated id
			assert (strcmp(userTab[i]->phone, userTab[k]->phone) != 0) ; // non repeated phone
		}
	}
	return true;
}

User* sql_selectOneRowFromTableWhere_user_phone(char* phone){
	for (int i = 0; i <= userTabCurIndex ; i++) {
			if (strcmp(userTab[i]->phone,phone)==0){
                return userTab[i];
            }
	}
	return NULL;
}

void sql_selectTable_user_print(){
    printf("sql_selectTable_user_print__[\n");
	for (int i = 0; i <= userTabCurIndex ; i++) {
        printRow_user(userTab[i],"sql_selectTable_user_print");
	}
    printf("]\n");
}
//}

//{ common assume : input field assume , included in java or : assuming in list not influence java execute result
bool assume_fieldInList_shopId(int shopId){
    if(shopId==FirstId){
        return true;
    }else
    if(shopId==FirstId+1){
        return true;
    }else
    // if(shopId==2){
        // return true;
    // }else
    if(shopId==FirstId+1+1){
        return true;
    }else
    {
        return false;
    }
}
//}

bool assume_fieldInList_activity_score(int score){
    if(score==Score1){
        return true;
    }else
    if(score==Score2){
        return true;
    }else
    if(score==ScoreNotValidated1){
        return false;
    }else
    if(score==ScoreNotValidated2){
        return false;
    }else
    {
        return false;
    }
}

//{ Activity assume : input field assume , included in java



bool assume_fieldInList_activity_name(Activity *pa){
    char* name=pa->name;
    if(strcmp(name,"Actv.1")==0){
        return true;
    }else
//    if(strcmp(name,"LiSi")==0){
//        return true;
//    }else
    if(strcmp(name,"Actv.2")==0){
        return true;
    }else{
        return false;
    }
}

bool assume_fieldInList_activity_shopId(Activity *p){
    return assume_fieldInList_shopId(p->shopId);
}


bool assume_fieldInList_activity_on(Activity *pa){
    bool on=pa->on;
    if(on==true){
        return true;
    }else
    if(on==false){
        return true;
    }else
    {
        return false;
    }
}

bool assume_fieldInList_activity_newUserScore(Activity *pa){
   return assume_fieldInList_activity_score(pa->newUserScore);
}

bool assume_fieldInList_activity_oldUserScore(Activity *pa){
   return assume_fieldInList_activity_score(pa->oldUserScore);
}



bool assume_betweenFields_activity_newOldUserScoreNotEqual(Activity *pActivity1){
    if(pActivity1->newUserScore != pActivity1->oldUserScore){
        return true;
    }else{
        return false;
    }
}

//}

//{ other 

//}


//{User service : simulate mysql.table and java insert sql
int service_save_row_user(User *pa) {
	if (userTabCurIndex >= TableMaxRow) {
		return ErrOutOfTableMaxRow;
	}
	userTabCurIndex++;
	userTabCurId++;
	pa->id = userTabCurId;
	userTab[userTabCurIndex] = pa;
	if (internalCheckTableValidated_user()==false) {
        printf("revert_service_save_row_user\n");
		userTabCurIndex--;
		userTabCurId--;
		return ErrBreakTableConstraint;
	}
	else {
		return OK;
	}
}



//}

//{Activity api : simulate mysql.table and java insert sql
bool api_save_row_activity(Activity *pa) {
	if (activityTabCurIndex >= TableMaxRow) {
		return ErrOutOfTableMaxRow;
	}
	activityTabCurIndex++;
	activityTabCurId++;
	pa->id = activityTabCurId;
	activityTab[activityTabCurIndex] = pa;
	if (internalCheckTableValidated_activity()==false) {
		activityTabCurIndex--;
		activityTabCurId--;
		return ErrBreakTableConstraint;
	}
	else {
		return OK;
	}
}

bool api_hasActivity(User* p,Activity** ppaReturn){
    Activity* pa = sql_selectOneRowFromTableWhere_activity_shopId(p->shopId);
    if(pa==NULL){
        return false;
    }
    if(pa->on==false){
        return false;
    }
    if(ppaReturn!=NULL){
        (*ppaReturn) = pa;
    }
    return true;    
}

int api_joinActivity(User* pUser){
    Activity* pActivity=NULL;
    User* pUserFromTab =NULL;
    
    bool hasActivity = api_hasActivity(pUser,&pActivity);
    if(hasActivity==false){
        return false;
    }
    assert(pActivity!=NULL);//internal error in api_hasActivity
    
    pUserFromTab = sql_selectOneRowFromTableWhere_user_phone(pUser->phone);
    // printRow_user(pUserFromTab,"pUserFromTab");
    // printRow_activity(pActivity,"pActivity_api_joinActivity");
    
    if(pUserFromTab==NULL){
        //service_save_row_user(pUser);
        return pActivity->newUserScore;
    }else{
    return pActivity->oldUserScore;    
    }
    
}


//}




//{ User assume : input field assume , included in java or : assuming in list not influence java execute result
bool assume_fieldInList_user_phone(User *p){
    char* phone=p->phone;
    if(strcmp(phone,"13000000000")==0){
        return true;
    }else
    if(strcmp(phone,"18688888888")==0){
        return true;
    }else{
        return false;
    }
}


bool assume_fieldInList_user_shopId(User *p){
    return assume_fieldInList_shopId(p->shopId);
}


//}




